\begin{tabbing}
$\forall$$A$:es\_realizer\{i:l\}. 
\\[0ex]($\uparrow$Rplus?($A$))
\\[0ex]$\Rightarrow$ sqequal(\=R{-}Feasible\=\{i:l\}\+\+
\\[0ex]($A$);
\-\\[0ex](R{-}Feasible\=\{i:l\}\+
\\[0ex](Rplus{-}left($A$))
\-\\[0ex]$\wedge$ R{-}Feasible\=\{i:l\}\+
\\[0ex](Rplus{-}right($A$))
\-\\[0ex]$\wedge$ R{-}compat\=\{i:l\}\+
\\[0ex](Rplus{-}left($A$); Rplus{-}right($A$))))
\-\-
\end{tabbing}